/* -*- Mode: C++; c-basic-offset: 2 -*- */

#ifndef __TERN_RACE_DETECTOR
#define __TERN_RACE_DETECTOR

#define MAX_THREADS (64)

#include "klee/ExecutionState.h"
#include <list>
#include <vector>
#include <ostream>
#include <string>

namespace klee {
  
  struct VectorClock {
    VectorClock(): width(0) {}

    void tick(int idx);
    void setWidth(int n);
    void merge(const VectorClock& vc);

    bool happensbefore(const VectorClock& vc) const;
    bool concurrent(const VectorClock& vc) const;
    void print(std::ostream &o);
    std::string toString();

    int clocks[MAX_THREADS], width;
  };
  

  /// Race-detection metadata for a particular memory access
  struct Access {
    Access(int t, bool i, const VectorClock& s, KInstruction *inst, 
           ref<Expr> v, ref<Expr> old_v);
    Access(const Access& a);

    int tid;
    bool isWrite;

    VectorClock ts; // vector clock of the access
    KInstruction *ki; // for debugging

    // value of the access
    ref<Expr> value; // value read or written
    ref<Expr> old_value; // value overwritten; undefined for read access


  };

  /// History of memory accesses for happens-before based race detection.
  /// Based on Dinning and Schonberg's paper "An Empirical Comparison of
  /// Monitoring Algorithms for Access Anomaly Detection", we don't have
  /// to remember all accesses; instead we need to remember only
  /// concurrent reads and one writes to avoid missing races.
  struct AccessHistory {
    AccessHistory(const MemoryObject *m, ref<Expr> o, int w);
    AccessHistory(const MemoryObject *m, ref<Expr> o, int w, Access *a);
    AccessHistory(const MemoryObject *m, long o, int w);
    AccessHistory(const MemoryObject *m, long o, int w, Access *a);
    AccessHistory(const AccessHistory& ah);
    ~AccessHistory();

    void printRace(Access *a1, Access *a2);
    /// remove reads < access->ts
    void removeReads(Access *access);
    bool appendAccess(Access *access);

    // memory object and range accessed
    const MemoryObject *mo;
    ref<Expr> offset;
    int width;

    /// concurrent reads to range [offset, offset+width)
    std::list<Access*> reads;
    /// existing write to range
    Access *write;
  };
  
  typedef ImmutableMap<long, AccessHistory*> ConcreteAccessMap;
  typedef std::list<AccessHistory*> SymbolicAccessList;

  class ObjectAccessHistory {
  public:
    ~ObjectAccessHistory();
    /// handle an access with an overlapping but not identical memory
    /// range to an existing access
    bool overlapRangeAccess(const MemoryObject *o, 
                            long off, int w, Access *access);
    bool appendAccess(const MemoryObject *o, ref<Expr> offset, 
                      int w, Access *access);

    /// Concrete memory accesses to this object
    ConcreteAccessMap concreteAccesses;
    /// Symbolic memory accesses to this object
    SymbolicAccessList symbolicAccesses;

  };

  typedef ImmutableMap<const MemoryObject*, ObjectAccessHistory*, MemoryObjectLT> ObjectAccessMap;

  class RaceDetector {
  public:
    RaceDetector();
    ~RaceDetector();

    void onMemoryAccess(ExecutionState &state, int tid, bool isWrite, 
                        const MemoryObject *mo, ref<Expr> offset, int width,
                        ref<Expr> value, ref<Expr> old_value);
    void onCreateThread(int parent_tid, int child_tid);
    void onAcquireTurn(int tid);
    void onReleaseTurn(int tid);
    bool raceDetected() {return racy;}

    /// memory accesses for all objects
    ObjectAccessMap objectAccesses;

    /// vector clocks for all threads
    VectorClock threadClocks[MAX_THREADS];

    /// vector clock of the turn token
    VectorClock turnClock;

    /// if current schedule is racy
    bool racy;
  };

  extern RaceDetector *theRaceDetector;
}

#endif // #define __TERN_RACE_DETECTOR
